Left Termination of the query pattern
palindrome(g)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 185 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 78 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇒, 0 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇒, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 PiDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇒, 0 ms)
        ↳25 QDP
        ↳26 QDPOrderProof (⇔, 67 ms)
        ↳27 QDP
        ↳28 PisEmptyProof (⇔, 0 ms)
        ↳29 YES

(0) Obligation:

Clauses:

palindrome(L) :- ','(halves(L, X1s, X2s, EvenOdd), ','(eq(EvenOdd, even), eq(X1s, X2s))).
palindrome(L) :- ','(halves(L, X1s, X2s, EvenOdd), ','(eq(EvenOdd, odd), last(X1s, X1, X2s))).
halves([], [], [], even).
halves(.(X, []), .(X, []), [], odd).
halves(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd) :- ','(last(.(Y, Xs), R, Rests), halves(Rests, Ts, Rs, EvenOdd)).
last(.(T, []), T, []).
last(.(H, T), X, .(H, M)) :- last(T, X, M).
eq(X, X).

Query: palindrome(g)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

lastA(.(X1, X2), X3, .(X1, X4)) :- lastA(X2, X3, X4).
lastB(X1, X2, X3, .(X1, X4)) :- lastA(X2, X3, X4).
halvesC(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7) :- lastB(X2, X3, X5, X8).
halvesC(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7) :- ','(lastcB(X2, X3, X5, X8), halvesC(X8, X4, X6, X7)).
lastD(.(X1, X2), X3, .(X1, X4)) :- lastD(X2, X3, X4).
palindromeE(.(X1, .(X2, X3))) :- lastB(X2, X3, X4, X5).
palindromeE(.(X1, .(X2, X3))) :- ','(lastcB(X2, X3, X4, X5), halvesC(X5, X6, X7, X8)).
palindromeE(X1) :- halvesC(X1, X2, X3, X4).
palindromeE(X1) :- ','(halvescC(X1, X2, X3, odd), lastD(X2, X4, X3)).

Clauses:

lastcA(.(X1, []), X1, []).
lastcA(.(X1, X2), X3, .(X1, X4)) :- lastcA(X2, X3, X4).
lastcB(X1, [], X1, []).
lastcB(X1, X2, X3, .(X1, X4)) :- lastcA(X2, X3, X4).
halvescC([], [], [], even).
halvescC(.(X1, []), .(X1, []), [], odd).
halvescC(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7) :- ','(lastcB(X2, X3, X5, X8), halvescC(X8, X4, X6, X7)).
lastcD(.(X1, []), X1, []).
lastcD(.(X1, X2), X3, .(X1, X4)) :- lastcD(X2, X3, X4).

Afs:

palindromeE(x1)  =  palindromeE(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
palindromeE_in: (b)
lastB_in: (b,b,f,f)
lastA_in: (b,f,f)
lastcB_in: (b,b,f,f)
lastcA_in: (b,f,f)
halvesC_in: (b,f,f,f)
halvescC_in: (b,f,f,b)
lastD_in: (b,f,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

PALINDROMEE_IN_G(.(X1, .(X2, X3))) → U7_G(X1, X2, X3, lastB_in_ggaa(X2, X3, X4, X5))
PALINDROMEE_IN_G(.(X1, .(X2, X3))) → LASTB_IN_GGAA(X2, X3, X4, X5)
LASTB_IN_GGAA(X1, X2, X3, .(X1, X4)) → U2_GGAA(X1, X2, X3, X4, lastA_in_gaa(X2, X3, X4))
LASTB_IN_GGAA(X1, X2, X3, .(X1, X4)) → LASTA_IN_GAA(X2, X3, X4)
LASTA_IN_GAA(.(X1, X2), X3, .(X1, X4)) → U1_GAA(X1, X2, X3, X4, lastA_in_gaa(X2, X3, X4))
LASTA_IN_GAA(.(X1, X2), X3, .(X1, X4)) → LASTA_IN_GAA(X2, X3, X4)
PALINDROMEE_IN_G(.(X1, .(X2, X3))) → U8_G(X1, X2, X3, lastcB_in_ggaa(X2, X3, X4, X5))
U8_G(X1, X2, X3, lastcB_out_ggaa(X2, X3, X4, X5)) → U9_G(X1, X2, X3, halvesC_in_gaaa(X5, X6, X7, X8))
U8_G(X1, X2, X3, lastcB_out_ggaa(X2, X3, X4, X5)) → HALVESC_IN_GAAA(X5, X6, X7, X8)
HALVESC_IN_GAAA(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7) → U3_GAAA(X1, X2, X3, X4, X5, X6, X7, lastB_in_ggaa(X2, X3, X5, X8))
HALVESC_IN_GAAA(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7) → LASTB_IN_GGAA(X2, X3, X5, X8)
HALVESC_IN_GAAA(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7) → U4_GAAA(X1, X2, X3, X4, X5, X6, X7, lastcB_in_ggaa(X2, X3, X5, X8))
U4_GAAA(X1, X2, X3, X4, X5, X6, X7, lastcB_out_ggaa(X2, X3, X5, X8)) → U5_GAAA(X1, X2, X3, X4, X5, X6, X7, halvesC_in_gaaa(X8, X4, X6, X7))
U4_GAAA(X1, X2, X3, X4, X5, X6, X7, lastcB_out_ggaa(X2, X3, X5, X8)) → HALVESC_IN_GAAA(X8, X4, X6, X7)
PALINDROMEE_IN_G(X1) → U10_G(X1, halvesC_in_gaaa(X1, X2, X3, X4))
PALINDROMEE_IN_G(X1) → HALVESC_IN_GAAA(X1, X2, X3, X4)
PALINDROMEE_IN_G(X1) → U11_G(X1, halvescC_in_gaag(X1, X2, X3, odd))
U11_G(X1, halvescC_out_gaag(X1, X2, X3, odd)) → U12_G(X1, lastD_in_gag(X2, X4, X3))
U11_G(X1, halvescC_out_gaag(X1, X2, X3, odd)) → LASTD_IN_GAG(X2, X4, X3)
LASTD_IN_GAG(.(X1, X2), X3, .(X1, X4)) → U6_GAG(X1, X2, X3, X4, lastD_in_gag(X2, X3, X4))
LASTD_IN_GAG(.(X1, X2), X3, .(X1, X4)) → LASTD_IN_GAG(X2, X3, X4)

The TRS R consists of the following rules:

lastcB_in_ggaa(X1, [], X1, []) → lastcB_out_ggaa(X1, [], X1, [])
lastcB_in_ggaa(X1, X2, X3, .(X1, X4)) → U15_ggaa(X1, X2, X3, X4, lastcA_in_gaa(X2, X3, X4))
lastcA_in_gaa(.(X1, []), X1, []) → lastcA_out_gaa(.(X1, []), X1, [])
lastcA_in_gaa(.(X1, X2), X3, .(X1, X4)) → U14_gaa(X1, X2, X3, X4, lastcA_in_gaa(X2, X3, X4))
U14_gaa(X1, X2, X3, X4, lastcA_out_gaa(X2, X3, X4)) → lastcA_out_gaa(.(X1, X2), X3, .(X1, X4))
U15_ggaa(X1, X2, X3, X4, lastcA_out_gaa(X2, X3, X4)) → lastcB_out_ggaa(X1, X2, X3, .(X1, X4))
halvescC_in_gaag([], [], [], even) → halvescC_out_gaag([], [], [], even)
halvescC_in_gaag(.(X1, []), .(X1, []), [], odd) → halvescC_out_gaag(.(X1, []), .(X1, []), [], odd)
halvescC_in_gaag(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7) → U16_gaag(X1, X2, X3, X4, X5, X6, X7, lastcB_in_ggaa(X2, X3, X5, X8))
U16_gaag(X1, X2, X3, X4, X5, X6, X7, lastcB_out_ggaa(X2, X3, X5, X8)) → U17_gaag(X1, X2, X3, X4, X5, X6, X7, halvescC_in_gaag(X8, X4, X6, X7))
U17_gaag(X1, X2, X3, X4, X5, X6, X7, halvescC_out_gaag(X8, X4, X6, X7)) → halvescC_out_gaag(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
lastB_in_ggaa(x1, x2, x3, x4)  =  lastB_in_ggaa(x1, x2)
lastA_in_gaa(x1, x2, x3)  =  lastA_in_gaa(x1)
lastcB_in_ggaa(x1, x2, x3, x4)  =  lastcB_in_ggaa(x1, x2)
[]  =  []
lastcB_out_ggaa(x1, x2, x3, x4)  =  lastcB_out_ggaa(x1, x2, x3, x4)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
lastcA_in_gaa(x1, x2, x3)  =  lastcA_in_gaa(x1)
lastcA_out_gaa(x1, x2, x3)  =  lastcA_out_gaa(x1, x2, x3)
U14_gaa(x1, x2, x3, x4, x5)  =  U14_gaa(x1, x2, x5)
halvesC_in_gaaa(x1, x2, x3, x4)  =  halvesC_in_gaaa(x1)
halvescC_in_gaag(x1, x2, x3, x4)  =  halvescC_in_gaag(x1, x4)
even  =  even
halvescC_out_gaag(x1, x2, x3, x4)  =  halvescC_out_gaag(x1, x2, x3, x4)
odd  =  odd
U16_gaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_gaag(x1, x2, x3, x7, x8)
U17_gaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U17_gaag(x1, x2, x3, x5, x7, x8)
lastD_in_gag(x1, x2, x3)  =  lastD_in_gag(x1, x3)
PALINDROMEE_IN_G(x1)  =  PALINDROMEE_IN_G(x1)
U7_G(x1, x2, x3, x4)  =  U7_G(x1, x2, x3, x4)
LASTB_IN_GGAA(x1, x2, x3, x4)  =  LASTB_IN_GGAA(x1, x2)
U2_GGAA(x1, x2, x3, x4, x5)  =  U2_GGAA(x1, x2, x5)
LASTA_IN_GAA(x1, x2, x3)  =  LASTA_IN_GAA(x1)
U1_GAA(x1, x2, x3, x4, x5)  =  U1_GAA(x1, x2, x5)
U8_G(x1, x2, x3, x4)  =  U8_G(x1, x2, x3, x4)
U9_G(x1, x2, x3, x4)  =  U9_G(x1, x2, x3, x4)
HALVESC_IN_GAAA(x1, x2, x3, x4)  =  HALVESC_IN_GAAA(x1)
U3_GAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U3_GAAA(x1, x2, x3, x8)
U4_GAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U4_GAAA(x1, x2, x3, x8)
U5_GAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U5_GAAA(x1, x2, x3, x8)
U10_G(x1, x2)  =  U10_G(x1, x2)
U11_G(x1, x2)  =  U11_G(x1, x2)
U12_G(x1, x2)  =  U12_G(x1, x2)
LASTD_IN_GAG(x1, x2, x3)  =  LASTD_IN_GAG(x1, x3)
U6_GAG(x1, x2, x3, x4, x5)  =  U6_GAG(x1, x2, x4, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PALINDROMEE_IN_G(.(X1, .(X2, X3))) → U7_G(X1, X2, X3, lastB_in_ggaa(X2, X3, X4, X5))
PALINDROMEE_IN_G(.(X1, .(X2, X3))) → LASTB_IN_GGAA(X2, X3, X4, X5)
LASTB_IN_GGAA(X1, X2, X3, .(X1, X4)) → U2_GGAA(X1, X2, X3, X4, lastA_in_gaa(X2, X3, X4))
LASTB_IN_GGAA(X1, X2, X3, .(X1, X4)) → LASTA_IN_GAA(X2, X3, X4)
LASTA_IN_GAA(.(X1, X2), X3, .(X1, X4)) → U1_GAA(X1, X2, X3, X4, lastA_in_gaa(X2, X3, X4))
LASTA_IN_GAA(.(X1, X2), X3, .(X1, X4)) → LASTA_IN_GAA(X2, X3, X4)
PALINDROMEE_IN_G(.(X1, .(X2, X3))) → U8_G(X1, X2, X3, lastcB_in_ggaa(X2, X3, X4, X5))
U8_G(X1, X2, X3, lastcB_out_ggaa(X2, X3, X4, X5)) → U9_G(X1, X2, X3, halvesC_in_gaaa(X5, X6, X7, X8))
U8_G(X1, X2, X3, lastcB_out_ggaa(X2, X3, X4, X5)) → HALVESC_IN_GAAA(X5, X6, X7, X8)
HALVESC_IN_GAAA(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7) → U3_GAAA(X1, X2, X3, X4, X5, X6, X7, lastB_in_ggaa(X2, X3, X5, X8))
HALVESC_IN_GAAA(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7) → LASTB_IN_GGAA(X2, X3, X5, X8)
HALVESC_IN_GAAA(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7) → U4_GAAA(X1, X2, X3, X4, X5, X6, X7, lastcB_in_ggaa(X2, X3, X5, X8))
U4_GAAA(X1, X2, X3, X4, X5, X6, X7, lastcB_out_ggaa(X2, X3, X5, X8)) → U5_GAAA(X1, X2, X3, X4, X5, X6, X7, halvesC_in_gaaa(X8, X4, X6, X7))
U4_GAAA(X1, X2, X3, X4, X5, X6, X7, lastcB_out_ggaa(X2, X3, X5, X8)) → HALVESC_IN_GAAA(X8, X4, X6, X7)
PALINDROMEE_IN_G(X1) → U10_G(X1, halvesC_in_gaaa(X1, X2, X3, X4))
PALINDROMEE_IN_G(X1) → HALVESC_IN_GAAA(X1, X2, X3, X4)
PALINDROMEE_IN_G(X1) → U11_G(X1, halvescC_in_gaag(X1, X2, X3, odd))
U11_G(X1, halvescC_out_gaag(X1, X2, X3, odd)) → U12_G(X1, lastD_in_gag(X2, X4, X3))
U11_G(X1, halvescC_out_gaag(X1, X2, X3, odd)) → LASTD_IN_GAG(X2, X4, X3)
LASTD_IN_GAG(.(X1, X2), X3, .(X1, X4)) → U6_GAG(X1, X2, X3, X4, lastD_in_gag(X2, X3, X4))
LASTD_IN_GAG(.(X1, X2), X3, .(X1, X4)) → LASTD_IN_GAG(X2, X3, X4)

The TRS R consists of the following rules:

lastcB_in_ggaa(X1, [], X1, []) → lastcB_out_ggaa(X1, [], X1, [])
lastcB_in_ggaa(X1, X2, X3, .(X1, X4)) → U15_ggaa(X1, X2, X3, X4, lastcA_in_gaa(X2, X3, X4))
lastcA_in_gaa(.(X1, []), X1, []) → lastcA_out_gaa(.(X1, []), X1, [])
lastcA_in_gaa(.(X1, X2), X3, .(X1, X4)) → U14_gaa(X1, X2, X3, X4, lastcA_in_gaa(X2, X3, X4))
U14_gaa(X1, X2, X3, X4, lastcA_out_gaa(X2, X3, X4)) → lastcA_out_gaa(.(X1, X2), X3, .(X1, X4))
U15_ggaa(X1, X2, X3, X4, lastcA_out_gaa(X2, X3, X4)) → lastcB_out_ggaa(X1, X2, X3, .(X1, X4))
halvescC_in_gaag([], [], [], even) → halvescC_out_gaag([], [], [], even)
halvescC_in_gaag(.(X1, []), .(X1, []), [], odd) → halvescC_out_gaag(.(X1, []), .(X1, []), [], odd)
halvescC_in_gaag(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7) → U16_gaag(X1, X2, X3, X4, X5, X6, X7, lastcB_in_ggaa(X2, X3, X5, X8))
U16_gaag(X1, X2, X3, X4, X5, X6, X7, lastcB_out_ggaa(X2, X3, X5, X8)) → U17_gaag(X1, X2, X3, X4, X5, X6, X7, halvescC_in_gaag(X8, X4, X6, X7))
U17_gaag(X1, X2, X3, X4, X5, X6, X7, halvescC_out_gaag(X8, X4, X6, X7)) → halvescC_out_gaag(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
lastB_in_ggaa(x1, x2, x3, x4)  =  lastB_in_ggaa(x1, x2)
lastA_in_gaa(x1, x2, x3)  =  lastA_in_gaa(x1)
lastcB_in_ggaa(x1, x2, x3, x4)  =  lastcB_in_ggaa(x1, x2)
[]  =  []
lastcB_out_ggaa(x1, x2, x3, x4)  =  lastcB_out_ggaa(x1, x2, x3, x4)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
lastcA_in_gaa(x1, x2, x3)  =  lastcA_in_gaa(x1)
lastcA_out_gaa(x1, x2, x3)  =  lastcA_out_gaa(x1, x2, x3)
U14_gaa(x1, x2, x3, x4, x5)  =  U14_gaa(x1, x2, x5)
halvesC_in_gaaa(x1, x2, x3, x4)  =  halvesC_in_gaaa(x1)
halvescC_in_gaag(x1, x2, x3, x4)  =  halvescC_in_gaag(x1, x4)
even  =  even
halvescC_out_gaag(x1, x2, x3, x4)  =  halvescC_out_gaag(x1, x2, x3, x4)
odd  =  odd
U16_gaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_gaag(x1, x2, x3, x7, x8)
U17_gaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U17_gaag(x1, x2, x3, x5, x7, x8)
lastD_in_gag(x1, x2, x3)  =  lastD_in_gag(x1, x3)
PALINDROMEE_IN_G(x1)  =  PALINDROMEE_IN_G(x1)
U7_G(x1, x2, x3, x4)  =  U7_G(x1, x2, x3, x4)
LASTB_IN_GGAA(x1, x2, x3, x4)  =  LASTB_IN_GGAA(x1, x2)
U2_GGAA(x1, x2, x3, x4, x5)  =  U2_GGAA(x1, x2, x5)
LASTA_IN_GAA(x1, x2, x3)  =  LASTA_IN_GAA(x1)
U1_GAA(x1, x2, x3, x4, x5)  =  U1_GAA(x1, x2, x5)
U8_G(x1, x2, x3, x4)  =  U8_G(x1, x2, x3, x4)
U9_G(x1, x2, x3, x4)  =  U9_G(x1, x2, x3, x4)
HALVESC_IN_GAAA(x1, x2, x3, x4)  =  HALVESC_IN_GAAA(x1)
U3_GAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U3_GAAA(x1, x2, x3, x8)
U4_GAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U4_GAAA(x1, x2, x3, x8)
U5_GAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U5_GAAA(x1, x2, x3, x8)
U10_G(x1, x2)  =  U10_G(x1, x2)
U11_G(x1, x2)  =  U11_G(x1, x2)
U12_G(x1, x2)  =  U12_G(x1, x2)
LASTD_IN_GAG(x1, x2, x3)  =  LASTD_IN_GAG(x1, x3)
U6_GAG(x1, x2, x3, x4, x5)  =  U6_GAG(x1, x2, x4, x5)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 17 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LASTD_IN_GAG(.(X1, X2), X3, .(X1, X4)) → LASTD_IN_GAG(X2, X3, X4)

The TRS R consists of the following rules:

lastcB_in_ggaa(X1, [], X1, []) → lastcB_out_ggaa(X1, [], X1, [])
lastcB_in_ggaa(X1, X2, X3, .(X1, X4)) → U15_ggaa(X1, X2, X3, X4, lastcA_in_gaa(X2, X3, X4))
lastcA_in_gaa(.(X1, []), X1, []) → lastcA_out_gaa(.(X1, []), X1, [])
lastcA_in_gaa(.(X1, X2), X3, .(X1, X4)) → U14_gaa(X1, X2, X3, X4, lastcA_in_gaa(X2, X3, X4))
U14_gaa(X1, X2, X3, X4, lastcA_out_gaa(X2, X3, X4)) → lastcA_out_gaa(.(X1, X2), X3, .(X1, X4))
U15_ggaa(X1, X2, X3, X4, lastcA_out_gaa(X2, X3, X4)) → lastcB_out_ggaa(X1, X2, X3, .(X1, X4))
halvescC_in_gaag([], [], [], even) → halvescC_out_gaag([], [], [], even)
halvescC_in_gaag(.(X1, []), .(X1, []), [], odd) → halvescC_out_gaag(.(X1, []), .(X1, []), [], odd)
halvescC_in_gaag(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7) → U16_gaag(X1, X2, X3, X4, X5, X6, X7, lastcB_in_ggaa(X2, X3, X5, X8))
U16_gaag(X1, X2, X3, X4, X5, X6, X7, lastcB_out_ggaa(X2, X3, X5, X8)) → U17_gaag(X1, X2, X3, X4, X5, X6, X7, halvescC_in_gaag(X8, X4, X6, X7))
U17_gaag(X1, X2, X3, X4, X5, X6, X7, halvescC_out_gaag(X8, X4, X6, X7)) → halvescC_out_gaag(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
lastcB_in_ggaa(x1, x2, x3, x4)  =  lastcB_in_ggaa(x1, x2)
[]  =  []
lastcB_out_ggaa(x1, x2, x3, x4)  =  lastcB_out_ggaa(x1, x2, x3, x4)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
lastcA_in_gaa(x1, x2, x3)  =  lastcA_in_gaa(x1)
lastcA_out_gaa(x1, x2, x3)  =  lastcA_out_gaa(x1, x2, x3)
U14_gaa(x1, x2, x3, x4, x5)  =  U14_gaa(x1, x2, x5)
halvescC_in_gaag(x1, x2, x3, x4)  =  halvescC_in_gaag(x1, x4)
even  =  even
halvescC_out_gaag(x1, x2, x3, x4)  =  halvescC_out_gaag(x1, x2, x3, x4)
odd  =  odd
U16_gaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_gaag(x1, x2, x3, x7, x8)
U17_gaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U17_gaag(x1, x2, x3, x5, x7, x8)
LASTD_IN_GAG(x1, x2, x3)  =  LASTD_IN_GAG(x1, x3)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LASTD_IN_GAG(.(X1, X2), X3, .(X1, X4)) → LASTD_IN_GAG(X2, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
LASTD_IN_GAG(x1, x2, x3)  =  LASTD_IN_GAG(x1, x3)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LASTD_IN_GAG(.(X1, X2), .(X1, X4)) → LASTD_IN_GAG(X2, X4)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LASTD_IN_GAG(.(X1, X2), .(X1, X4)) → LASTD_IN_GAG(X2, X4)
    The graph contains the following edges 1 > 1, 2 > 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LASTA_IN_GAA(.(X1, X2), X3, .(X1, X4)) → LASTA_IN_GAA(X2, X3, X4)

The TRS R consists of the following rules:

lastcB_in_ggaa(X1, [], X1, []) → lastcB_out_ggaa(X1, [], X1, [])
lastcB_in_ggaa(X1, X2, X3, .(X1, X4)) → U15_ggaa(X1, X2, X3, X4, lastcA_in_gaa(X2, X3, X4))
lastcA_in_gaa(.(X1, []), X1, []) → lastcA_out_gaa(.(X1, []), X1, [])
lastcA_in_gaa(.(X1, X2), X3, .(X1, X4)) → U14_gaa(X1, X2, X3, X4, lastcA_in_gaa(X2, X3, X4))
U14_gaa(X1, X2, X3, X4, lastcA_out_gaa(X2, X3, X4)) → lastcA_out_gaa(.(X1, X2), X3, .(X1, X4))
U15_ggaa(X1, X2, X3, X4, lastcA_out_gaa(X2, X3, X4)) → lastcB_out_ggaa(X1, X2, X3, .(X1, X4))
halvescC_in_gaag([], [], [], even) → halvescC_out_gaag([], [], [], even)
halvescC_in_gaag(.(X1, []), .(X1, []), [], odd) → halvescC_out_gaag(.(X1, []), .(X1, []), [], odd)
halvescC_in_gaag(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7) → U16_gaag(X1, X2, X3, X4, X5, X6, X7, lastcB_in_ggaa(X2, X3, X5, X8))
U16_gaag(X1, X2, X3, X4, X5, X6, X7, lastcB_out_ggaa(X2, X3, X5, X8)) → U17_gaag(X1, X2, X3, X4, X5, X6, X7, halvescC_in_gaag(X8, X4, X6, X7))
U17_gaag(X1, X2, X3, X4, X5, X6, X7, halvescC_out_gaag(X8, X4, X6, X7)) → halvescC_out_gaag(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
lastcB_in_ggaa(x1, x2, x3, x4)  =  lastcB_in_ggaa(x1, x2)
[]  =  []
lastcB_out_ggaa(x1, x2, x3, x4)  =  lastcB_out_ggaa(x1, x2, x3, x4)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
lastcA_in_gaa(x1, x2, x3)  =  lastcA_in_gaa(x1)
lastcA_out_gaa(x1, x2, x3)  =  lastcA_out_gaa(x1, x2, x3)
U14_gaa(x1, x2, x3, x4, x5)  =  U14_gaa(x1, x2, x5)
halvescC_in_gaag(x1, x2, x3, x4)  =  halvescC_in_gaag(x1, x4)
even  =  even
halvescC_out_gaag(x1, x2, x3, x4)  =  halvescC_out_gaag(x1, x2, x3, x4)
odd  =  odd
U16_gaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_gaag(x1, x2, x3, x7, x8)
U17_gaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U17_gaag(x1, x2, x3, x5, x7, x8)
LASTA_IN_GAA(x1, x2, x3)  =  LASTA_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LASTA_IN_GAA(.(X1, X2), X3, .(X1, X4)) → LASTA_IN_GAA(X2, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
LASTA_IN_GAA(x1, x2, x3)  =  LASTA_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LASTA_IN_GAA(.(X1, X2)) → LASTA_IN_GAA(X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LASTA_IN_GAA(.(X1, X2)) → LASTA_IN_GAA(X2)
    The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

HALVESC_IN_GAAA(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7) → U4_GAAA(X1, X2, X3, X4, X5, X6, X7, lastcB_in_ggaa(X2, X3, X5, X8))
U4_GAAA(X1, X2, X3, X4, X5, X6, X7, lastcB_out_ggaa(X2, X3, X5, X8)) → HALVESC_IN_GAAA(X8, X4, X6, X7)

The TRS R consists of the following rules:

lastcB_in_ggaa(X1, [], X1, []) → lastcB_out_ggaa(X1, [], X1, [])
lastcB_in_ggaa(X1, X2, X3, .(X1, X4)) → U15_ggaa(X1, X2, X3, X4, lastcA_in_gaa(X2, X3, X4))
lastcA_in_gaa(.(X1, []), X1, []) → lastcA_out_gaa(.(X1, []), X1, [])
lastcA_in_gaa(.(X1, X2), X3, .(X1, X4)) → U14_gaa(X1, X2, X3, X4, lastcA_in_gaa(X2, X3, X4))
U14_gaa(X1, X2, X3, X4, lastcA_out_gaa(X2, X3, X4)) → lastcA_out_gaa(.(X1, X2), X3, .(X1, X4))
U15_ggaa(X1, X2, X3, X4, lastcA_out_gaa(X2, X3, X4)) → lastcB_out_ggaa(X1, X2, X3, .(X1, X4))
halvescC_in_gaag([], [], [], even) → halvescC_out_gaag([], [], [], even)
halvescC_in_gaag(.(X1, []), .(X1, []), [], odd) → halvescC_out_gaag(.(X1, []), .(X1, []), [], odd)
halvescC_in_gaag(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7) → U16_gaag(X1, X2, X3, X4, X5, X6, X7, lastcB_in_ggaa(X2, X3, X5, X8))
U16_gaag(X1, X2, X3, X4, X5, X6, X7, lastcB_out_ggaa(X2, X3, X5, X8)) → U17_gaag(X1, X2, X3, X4, X5, X6, X7, halvescC_in_gaag(X8, X4, X6, X7))
U17_gaag(X1, X2, X3, X4, X5, X6, X7, halvescC_out_gaag(X8, X4, X6, X7)) → halvescC_out_gaag(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
lastcB_in_ggaa(x1, x2, x3, x4)  =  lastcB_in_ggaa(x1, x2)
[]  =  []
lastcB_out_ggaa(x1, x2, x3, x4)  =  lastcB_out_ggaa(x1, x2, x3, x4)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
lastcA_in_gaa(x1, x2, x3)  =  lastcA_in_gaa(x1)
lastcA_out_gaa(x1, x2, x3)  =  lastcA_out_gaa(x1, x2, x3)
U14_gaa(x1, x2, x3, x4, x5)  =  U14_gaa(x1, x2, x5)
halvescC_in_gaag(x1, x2, x3, x4)  =  halvescC_in_gaag(x1, x4)
even  =  even
halvescC_out_gaag(x1, x2, x3, x4)  =  halvescC_out_gaag(x1, x2, x3, x4)
odd  =  odd
U16_gaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_gaag(x1, x2, x3, x7, x8)
U17_gaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U17_gaag(x1, x2, x3, x5, x7, x8)
HALVESC_IN_GAAA(x1, x2, x3, x4)  =  HALVESC_IN_GAAA(x1)
U4_GAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U4_GAAA(x1, x2, x3, x8)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

HALVESC_IN_GAAA(.(X1, .(X2, X3)), .(X1, X4), .(X5, X6), X7) → U4_GAAA(X1, X2, X3, X4, X5, X6, X7, lastcB_in_ggaa(X2, X3, X5, X8))
U4_GAAA(X1, X2, X3, X4, X5, X6, X7, lastcB_out_ggaa(X2, X3, X5, X8)) → HALVESC_IN_GAAA(X8, X4, X6, X7)

The TRS R consists of the following rules:

lastcB_in_ggaa(X1, [], X1, []) → lastcB_out_ggaa(X1, [], X1, [])
lastcB_in_ggaa(X1, X2, X3, .(X1, X4)) → U15_ggaa(X1, X2, X3, X4, lastcA_in_gaa(X2, X3, X4))
U15_ggaa(X1, X2, X3, X4, lastcA_out_gaa(X2, X3, X4)) → lastcB_out_ggaa(X1, X2, X3, .(X1, X4))
lastcA_in_gaa(.(X1, []), X1, []) → lastcA_out_gaa(.(X1, []), X1, [])
lastcA_in_gaa(.(X1, X2), X3, .(X1, X4)) → U14_gaa(X1, X2, X3, X4, lastcA_in_gaa(X2, X3, X4))
U14_gaa(X1, X2, X3, X4, lastcA_out_gaa(X2, X3, X4)) → lastcA_out_gaa(.(X1, X2), X3, .(X1, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
lastcB_in_ggaa(x1, x2, x3, x4)  =  lastcB_in_ggaa(x1, x2)
[]  =  []
lastcB_out_ggaa(x1, x2, x3, x4)  =  lastcB_out_ggaa(x1, x2, x3, x4)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
lastcA_in_gaa(x1, x2, x3)  =  lastcA_in_gaa(x1)
lastcA_out_gaa(x1, x2, x3)  =  lastcA_out_gaa(x1, x2, x3)
U14_gaa(x1, x2, x3, x4, x5)  =  U14_gaa(x1, x2, x5)
HALVESC_IN_GAAA(x1, x2, x3, x4)  =  HALVESC_IN_GAAA(x1)
U4_GAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U4_GAAA(x1, x2, x3, x8)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

HALVESC_IN_GAAA(.(X1, .(X2, X3))) → U4_GAAA(X1, X2, X3, lastcB_in_ggaa(X2, X3))
U4_GAAA(X1, X2, X3, lastcB_out_ggaa(X2, X3, X5, X8)) → HALVESC_IN_GAAA(X8)

The TRS R consists of the following rules:

lastcB_in_ggaa(X1, []) → lastcB_out_ggaa(X1, [], X1, [])
lastcB_in_ggaa(X1, X2) → U15_ggaa(X1, X2, lastcA_in_gaa(X2))
U15_ggaa(X1, X2, lastcA_out_gaa(X2, X3, X4)) → lastcB_out_ggaa(X1, X2, X3, .(X1, X4))
lastcA_in_gaa(.(X1, [])) → lastcA_out_gaa(.(X1, []), X1, [])
lastcA_in_gaa(.(X1, X2)) → U14_gaa(X1, X2, lastcA_in_gaa(X2))
U14_gaa(X1, X2, lastcA_out_gaa(X2, X3, X4)) → lastcA_out_gaa(.(X1, X2), X3, .(X1, X4))

The set Q consists of the following terms:

lastcB_in_ggaa(x0, x1)
U15_ggaa(x0, x1, x2)
lastcA_in_gaa(x0)
U14_gaa(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(26) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


HALVESC_IN_GAAA(.(X1, .(X2, X3))) → U4_GAAA(X1, X2, X3, lastcB_in_ggaa(X2, X3))
U4_GAAA(X1, X2, X3, lastcB_out_ggaa(X2, X3, X5, X8)) → HALVESC_IN_GAAA(X8)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + x2   
POL(HALVESC_IN_GAAA(x1)) = x1   
POL(U14_gaa(x1, x2, x3)) = 1 + x3   
POL(U15_ggaa(x1, x2, x3)) = 1 + x3   
POL(U4_GAAA(x1, x2, x3, x4)) = x4   
POL([]) = 1   
POL(lastcA_in_gaa(x1)) = x1   
POL(lastcA_out_gaa(x1, x2, x3)) = 1 + x3   
POL(lastcB_in_ggaa(x1, x2)) = 1 + x2   
POL(lastcB_out_ggaa(x1, x2, x3, x4)) = 1 + x4   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

lastcB_in_ggaa(X1, []) → lastcB_out_ggaa(X1, [], X1, [])
lastcB_in_ggaa(X1, X2) → U15_ggaa(X1, X2, lastcA_in_gaa(X2))
lastcA_in_gaa(.(X1, [])) → lastcA_out_gaa(.(X1, []), X1, [])
lastcA_in_gaa(.(X1, X2)) → U14_gaa(X1, X2, lastcA_in_gaa(X2))
U15_ggaa(X1, X2, lastcA_out_gaa(X2, X3, X4)) → lastcB_out_ggaa(X1, X2, X3, .(X1, X4))
U14_gaa(X1, X2, lastcA_out_gaa(X2, X3, X4)) → lastcA_out_gaa(.(X1, X2), X3, .(X1, X4))

(27) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

lastcB_in_ggaa(X1, []) → lastcB_out_ggaa(X1, [], X1, [])
lastcB_in_ggaa(X1, X2) → U15_ggaa(X1, X2, lastcA_in_gaa(X2))
U15_ggaa(X1, X2, lastcA_out_gaa(X2, X3, X4)) → lastcB_out_ggaa(X1, X2, X3, .(X1, X4))
lastcA_in_gaa(.(X1, [])) → lastcA_out_gaa(.(X1, []), X1, [])
lastcA_in_gaa(.(X1, X2)) → U14_gaa(X1, X2, lastcA_in_gaa(X2))
U14_gaa(X1, X2, lastcA_out_gaa(X2, X3, X4)) → lastcA_out_gaa(.(X1, X2), X3, .(X1, X4))

The set Q consists of the following terms:

lastcB_in_ggaa(x0, x1)
U15_ggaa(x0, x1, x2)
lastcA_in_gaa(x0)
U14_gaa(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(28) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(29) YES